ds:x:Id fp Type, da:k:Knd fp Type. event-info(ds;da)  Type 

latex

Definitions	Id, t  T, x. t(x), x:A. B(x), a:A fp B(a), Knd, Top, KindDeq, f(x)?z, State(ds), event-info(ds;da)
Lemmas	decl-state wf, fpf-cap wf, Kind-deq wf, top wf, Knd wf, fpf wf, Id wf